Termination w.r.t. Q proof of /tmp/tmpMo3Hxc/parting04_maxsort

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

Q is empty.

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
MAX(cons(x, cons(y, xs))) → GE(x, y)
IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF2(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
SORT(cons(x, xs)) → MAX(cons(x, xs))
SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))
SORT(cons(x, xs)) → H(del(max(cons(x, xs)), cons(x, xs)))
SORT(cons(x, xs)) → DEL(max(cons(x, xs)), cons(x, xs))
GE(s(x), s(y)) → GE(x, y)
H(cons(x, xs)) → H(xs)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
MAX(cons(x, cons(y, xs))) → GE(x, y)
IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF2(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
SORT(cons(x, xs)) → MAX(cons(x, xs))
SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))
SORT(cons(x, xs)) → H(del(max(cons(x, xs)), cons(x, xs)))
SORT(cons(x, xs)) → DEL(max(cons(x, xs)), cons(x, xs))
GE(s(x), s(y)) → GE(x, y)
H(cons(x, xs)) → H(xs)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 5 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(cons(x, xs)) → H(xs)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(cons(x, xs)) → H(xs)

R is empty.
The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(cons(x, xs)) → H(xs)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

H(cons(x, xs)) → H(xs)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

From the DPs we obtained the following set of size-change graphs:

GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

From the DPs we obtained the following set of size-change graphs:

EQ(s(x), s(y)) → EQ(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2(false, x, y, xs) → DEL(x, xs)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)

The remaining pairs can at least be oriented weakly.

IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(IF1(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(MAX(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(s(x₁)) = 0
POL(true) = 0

The following usable rules [FROCOS05] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))

The TRS R consists of the following rules:

max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

sort(nil)
sort(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))

The TRS R consists of the following rules:

max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.

This DP could be deleted by the Induction-Processor:
SORT(cons(x', xs')) → SORT(h(del(max(cons(x', xs')), cons(x', xs'))))

This order was computed:
Polynomial interpretation [POLO]:

POL(0) = 0
POL(SORT(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(del(x₁, x₂)) = x₂
POL(eq(x₁, x₂)) = 1
POL(false) = 0
POL(ge(x₁, x₂)) = 1
POL(h(x₁)) = x₁
POL(if1(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + 2·x₂ + 2·x₃ + 3·x₄
POL(if2(x₁, x₂, x₃, x₄)) = 1 + 2·x₃ + 2·x₄
POL(max(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 1

At least one of these decreasing rules is always used after the deleted DP:
if2(true, x1609, y1039, xs809) → xs809

The following formula is valid:
z0:sort[a36].(¬(z0 =nil)→del'(max(z0 ), z0 )=true)

The transformed set:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                              ↳ PisEmptyProof

                            ↳ QTRS

Q DP problem:
P is empty.
The TRS R consists of the following rules:

max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

Q is empty.

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
DEL'(x58, cons(y37, xs29)) → EQ(x58, y37)
IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
MAX(cons(x13, cons(y7, xs5))) → GE(x13, y7)
IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
DEL(x58, cons(y37, xs29)) → EQ(x58, y37)
H(cons(x87, xs44)) → H(xs44)
EQ(s(x145), s(y93)) → EQ(x145, y93)
IF2(false, x175, y113, xs88) → DEL(x175, xs88)
GE(s(x249), s(y159)) → GE(x249, y159)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
DEL'(x58, cons(y37, xs29)) → EQ(x58, y37)
IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
MAX(cons(x13, cons(y7, xs5))) → GE(x13, y7)
IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
DEL(x58, cons(y37, xs29)) → EQ(x58, y37)
H(cons(x87, xs44)) → H(xs44)
EQ(s(x145), s(y93)) → EQ(x145, y93)
IF2(false, x175, y113, xs88) → DEL(x175, xs88)
GE(s(x249), s(y159)) → GE(x249, y159)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 4 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)

R is empty.
The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPSizeChangeProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)

From the DPs we obtained the following set of size-change graphs:

EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
The graph contains the following edges 1 > 1, 2 > 2
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)

R is empty.
The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPSizeChangeProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)

From the DPs we obtained the following set of size-change graphs:

EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x249), s(y159)) → GE(x249, y159)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x249), s(y159)) → GE(x249, y159)

R is empty.
The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPSizeChangeProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x249), s(y159)) → GE(x249, y159)

From the DPs we obtained the following set of size-change graphs:

GE(s(x249), s(y159)) → GE(x249, y159)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x145), s(y93)) → EQ(x145, y93)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x145), s(y93)) → EQ(x145, y93)

R is empty.
The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPSizeChangeProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x145), s(y93)) → EQ(x145, y93)

From the DPs we obtained the following set of size-change graphs:

EQ(s(x145), s(y93)) → EQ(x145, y93)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(cons(x87, xs44)) → H(xs44)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(cons(x87, xs44)) → H(xs44)

R is empty.
The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPSizeChangeProof

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

H(cons(x87, xs44)) → H(xs44)

From the DPs we obtained the following set of size-change graphs:

H(cons(x87, xs44)) → H(xs44)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x175, y113, xs88) → DEL(x175, xs88)
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x175, y113, xs88) → DEL(x175, xs88)
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPSizeChangeProof

                                          ↳ QDP

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x175, y113, xs88) → DEL(x175, xs88)
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))

From the DPs we obtained the following set of size-change graphs:

DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2(false, x175, y113, xs88) → DEL(x175, xs88)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))

The TRS R consists of the following rules:

ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))

The TRS R consists of the following rules:

ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)

The set Q consists of the following terms:

ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)

The remaining pairs can at least be oriented weakly.

IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(IF1(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(MAX(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(s(x₁)) = 0
POL(true) = 0

The following usable rules [FROCOS05] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))

The TRS R consists of the following rules:

ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)

The set Q consists of the following terms:

ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)

The TRS R consists of the following rules:

del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x', nil)) → x'
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)

The set Q consists of the following terms:

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Induction-Processor

                          ↳ AND

                            ↳ QDP

                            ↳ QTRS

                              ↳ Overlay + Local Confluence

                                ↳ QTRS

                                  ↳ DependencyPairsProof

                                    ↳ QDP

                                      ↳ DependencyGraphProof

                                        ↳ AND

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))

From the DPs we obtained the following set of size-change graphs:

DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
The graph contains the following edges 2 >= 1, 4 >= 2